home *** CD-ROM | disk | FTP | other *** search
/ Turnbull China Bikeride / Turnbull China Bikeride - Disc 1.iso / ARGONET / PD / PROGRAMMING / LCLINT2.SPK / test / test_b / c / spccluses2 < prev    next >
Text File  |  1996-08-28  |  2KB  |  77 lines
  1. /*@-paramuse@*/
  2.  
  3. typedef struct
  4. {
  5.   char *name;
  6.   char *id;
  7.   int year;
  8. } record;
  9.  
  10. extern void allocYear (/*@special@*/ record *r)
  11.   /*@allocates r->year@*/  /* 1. Allocates clause includes *<parameter 1>.year of ... */
  12. {
  13.   r->year = 23;
  14. } /* 2. Unallocated storage r->year corresponds to storage listed ... */
  15.  
  16. extern void setName (/*@special@*/ record *r, /*@only@*/ char *name)
  17.   /*@defines r->name@*/ 
  18. {
  19.   r->name = name;
  20. }
  21.  
  22. extern void setName1 (/*@special@*/ record *r, /*@only@*/ char *name)
  23.   /*@defines r->name@*/ 
  24. {
  25.   free (name);
  26. } /* 3. Storage r->name listed in defines clause not defined at ... */
  27.  
  28. extern void setName2 (/*@special@*/ record *r, char *name)
  29.   /*@sets r->name@*/ 
  30. {
  31.   strcpy (r->name, name);
  32. }
  33.  
  34. extern void setName3 (/*@special@*/ record *r, char *name)
  35.   /*@sets r->name@*/ 
  36. {
  37. } /* 4. Storage *(r->name) listed in sets clause not defined at ... */
  38.  
  39. extern void setName4 (/*@special@*/ record *r, /*@only@*/ char *name)
  40.   /*@sets r->name@*/ 
  41. {
  42.   r->name = name; /* 5. Implicitly only storage r->name not released before ... */
  43. }
  44.  
  45. extern void allocName (/*@special@*/ record *r)
  46.   /*@allocates r->name@*/ 
  47. {
  48.   r->name = (char *) malloc (sizeof (char) * 20);
  49. }
  50.  
  51. extern void allocName2 (/*@special@*/ record *r)
  52.   /*@allocates r->name@*/ 
  53. {
  54. } /* 6. Storage r->name listed in allocates clauses is not ... */
  55.  
  56. extern void freeName (/*@special@*/ record r)
  57.   /*@releases r.name@*/
  58. {
  59.   free (r.name); 
  60. }
  61.  
  62. extern void freeName2 (/*@special@*/ record r)
  63.   /*@releases r.name@*/
  64. {
  65. } /* 7. Storage r.name listed in releases clause not released */
  66.  
  67. extern void freeName3 (/*@special@*/ record *r)
  68.   /*@releases r->name@*/
  69. {
  70.   free (r->name);
  71. }
  72.  
  73. extern void freeName4 (/*@special@*/ record *r)
  74.   /*@releases r->name@*/
  75. {
  76. } /* 8. Storage r->name listed in releases clause not released ... */
  77.